\begin{tabbing}
$\forall$$A$,$B$:es\_realizer\{i:l\}.
\\[0ex]R{-}compat\=\{i:l\}\+
\\[0ex]($A$; $B$)
\-\\[0ex]$\Rightarrow$ ($\forall$$i$:Id. fpf{-}compatible(Knd; $x$.Type; Kind{-}deq; R{-}da($A$; $i$); R{-}da($B$; $i$)))
\end{tabbing}